T:Type, L1,L2:(T List), x,y:T.
((y  L2))  l_before(x; y; append(L1; L2); T)  l_before(x; y; L1; T) 

latex

Definitions	ff, tt, i <z j, b, tl(l), i z j, if b then t else f fi , nth_tl(n;as), hd(l), Y, ||as||, l[i], t  T, last(L), l_before(x; y; l; T), P  Q, x:A. B(x), guard(T), prop{i:l}
Lemmas	l member wf, append wf, sublist wf, null wf, assert wf, not wf, sublist append front